p, q:. (p  q)   

latex

ProofTree

Definitions	p  q, t  T, x:A. B(x)
Lemmas	bool wf, bfalse wf, ifthenelse wf